0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 40 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 10.8 s)
↳10 BOUNDS(1, n^3)
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x, y) → div2(x, y, 0) [1]
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i)) [1]
if1(true, b, x, y, i, j) → divZeroError [1]
if1(false, b, x, y, i, j) → if2(b, x, y, i, j) [1]
if2(true, x, y, i, j) → div2(minus(x, y), y, j) [1]
if2(false, x, y, i, j) → i [1]
inc(0) → 0 [1]
inc(s(i)) → s(inc(i)) [1]
le(s(x), 0) → false [1]
le(0, y) → true [1]
le(s(x), s(y)) → le(x, y) [1]
minus(x, 0) → x [1]
minus(0, y) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
plus(x, y) → plusIter(x, y, 0) [1]
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z) [1]
ifPlus(true, x, y, z) → y [1]
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z)) [1]
a → c [1]
a → d [1]
div(x, y) → div2(x, y, 0) [1]
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i)) [1]
if1(true, b, x, y, i, j) → divZeroError [1]
if1(false, b, x, y, i, j) → if2(b, x, y, i, j) [1]
if2(true, x, y, i, j) → div2(minus(x, y), y, j) [1]
if2(false, x, y, i, j) → i [1]
inc(0) → 0 [1]
inc(s(i)) → s(inc(i)) [1]
le(s(x), 0) → false [1]
le(0, y) → true [1]
le(s(x), s(y)) → le(x, y) [1]
minus(x, 0) → x [1]
minus(0, y) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
plus(x, y) → plusIter(x, y, 0) [1]
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z) [1]
ifPlus(true, x, y, z) → y [1]
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z)) [1]
a → c [1]
a → d [1]
| div :: 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s div2 :: 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s 0 :: 0:divZeroError:s if1 :: true:false → true:false → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s le :: 0:divZeroError:s → 0:divZeroError:s → true:false plus :: 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s inc :: 0:divZeroError:s → 0:divZeroError:s true :: true:false divZeroError :: 0:divZeroError:s false :: true:false if2 :: true:false → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s minus :: 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s s :: 0:divZeroError:s → 0:divZeroError:s plusIter :: 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s ifPlus :: true:false → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s → 0:divZeroError:s a :: c:d c :: c:d d :: c:d |
inc(v0) → null_inc [0]
le(v0, v1) → null_le [0]
minus(v0, v1) → null_minus [0]
if1(v0, v1, v2, v3, v4, v5) → null_if1 [0]
if2(v0, v1, v2, v3, v4) → null_if2 [0]
ifPlus(v0, v1, v2, v3) → null_ifPlus [0]
null_inc, null_le, null_minus, null_if1, null_if2, null_ifPlus
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 2
divZeroError => 1
false => 1
c => 0
d => 1
null_inc => 0
null_le => 0
null_minus => 0
null_if1 => 0
null_if2 => 0
null_ifPlus => 0
a -{ 1 }→ 1 :|:
a -{ 1 }→ 0 :|:
div(z', z'') -{ 1 }→ div2(x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0
div2(z', z'', z1) -{ 1 }→ if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i)) :|: z' = x, z'' = y, x >= 0, y >= 0, i >= 0, z1 = i
if1(z', z'', z1, z2, z3, z4) -{ 1 }→ if2(b, x, y, i, j) :|: b >= 0, j >= 0, z2 = y, z'' = b, z3 = i, z4 = j, x >= 0, y >= 0, i >= 0, z' = 1, z1 = x
if1(z', z'', z1, z2, z3, z4) -{ 1 }→ 1 :|: b >= 0, j >= 0, z2 = y, z'' = b, z' = 2, z3 = i, z4 = j, x >= 0, y >= 0, i >= 0, z1 = x
if1(z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z2 = v3, z4 = v5, v0 >= 0, v4 >= 0, z1 = v2, v1 >= 0, v5 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0
if2(z', z'', z1, z2, z3) -{ 1 }→ i :|: j >= 0, z1 = y, z2 = i, x >= 0, y >= 0, z3 = j, i >= 0, z'' = x, z' = 1
if2(z', z'', z1, z2, z3) -{ 1 }→ div2(minus(x, y), y, j) :|: j >= 0, z1 = y, z2 = i, z' = 2, x >= 0, y >= 0, z3 = j, i >= 0, z'' = x
if2(z', z'', z1, z2, z3) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, v4 >= 0, z1 = v2, v1 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0
ifPlus(z', z'', z1, z2) -{ 1 }→ y :|: z1 = y, z >= 0, z' = 2, z2 = z, x >= 0, y >= 0, z'' = x
ifPlus(z', z'', z1, z2) -{ 1 }→ plusIter(x, 1 + y, 1 + z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
ifPlus(z', z'', z1, z2) -{ 0 }→ 0 :|: z2 = v3, v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, v3 >= 0, z' = v0
inc(z') -{ 1 }→ 0 :|: z' = 0
inc(z') -{ 0 }→ 0 :|: v0 >= 0, z' = v0
inc(z') -{ 1 }→ 1 + inc(i) :|: z' = 1 + i, i >= 0
le(z', z'') -{ 1 }→ le(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
le(z', z'') -{ 1 }→ 2 :|: z'' = y, y >= 0, z' = 0
le(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = 1 + x, x >= 0
le(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
minus(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
minus(z', z'') -{ 1 }→ minus(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
minus(z', z'') -{ 1 }→ 0 :|: z'' = y, y >= 0, z' = 0
minus(z', z'') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0
plus(z', z'') -{ 1 }→ plusIter(x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0
plusIter(z', z'', z1) -{ 1 }→ ifPlus(le(x, z), x, y, z) :|: z1 = z, z >= 0, z' = x, z'' = y, x >= 0, y >= 0
| eq(start(V, V1, V4, V8, V9, V10),0,[div(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[div2(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[if1(V, V1, V4, V8, V9, V10, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[if2(V, V1, V4, V8, V9, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0,V9 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[inc(V, Out)],[V >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[plusIter(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[ifPlus(V, V1, V4, V8, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0]). eq(start(V, V1, V4, V8, V9, V10),0,[a(Out)],[]). eq(div(V, V1, Out),1,[div2(V2, V3, 0, Ret)],[Out = Ret,V = V2,V1 = V3,V2 >= 0,V3 >= 0]). eq(div2(V, V1, V4, Out),1,[le(V5, 0, Ret0),le(V5, V6, Ret1),plus(V7, 0, Ret4),inc(V7, Ret5),if1(Ret0, Ret1, V6, V5, Ret4, Ret5, Ret2)],[Out = Ret2,V = V6,V1 = V5,V6 >= 0,V5 >= 0,V7 >= 0,V4 = V7]). eq(if1(V, V1, V4, V8, V9, V10, Out),1,[],[Out = 1,V11 >= 0,V12 >= 0,V8 = V13,V1 = V11,V = 2,V9 = V14,V10 = V12,V15 >= 0,V13 >= 0,V14 >= 0,V4 = V15]). eq(if1(V, V1, V4, V8, V9, V10, Out),1,[if2(V16, V17, V18, V19, V20, Ret3)],[Out = Ret3,V16 >= 0,V20 >= 0,V8 = V18,V1 = V16,V9 = V19,V10 = V20,V17 >= 0,V18 >= 0,V19 >= 0,V = 1,V4 = V17]). eq(if2(V, V1, V4, V8, V9, Out),1,[minus(V21, V22, Ret01),div2(Ret01, V22, V23, Ret6)],[Out = Ret6,V23 >= 0,V4 = V22,V8 = V24,V = 2,V21 >= 0,V22 >= 0,V9 = V23,V24 >= 0,V1 = V21]). eq(if2(V, V1, V4, V8, V9, Out),1,[],[Out = V25,V26 >= 0,V4 = V27,V8 = V25,V28 >= 0,V27 >= 0,V9 = V26,V25 >= 0,V1 = V28,V = 1]). eq(inc(V, Out),1,[],[Out = 0,V = 0]). eq(inc(V, Out),1,[inc(V29, Ret11)],[Out = 1 + Ret11,V = 1 + V29,V29 >= 0]). eq(le(V, V1, Out),1,[],[Out = 1,V1 = 0,V = 1 + V30,V30 >= 0]). eq(le(V, V1, Out),1,[],[Out = 2,V1 = V31,V31 >= 0,V = 0]). eq(le(V, V1, Out),1,[le(V32, V33, Ret7)],[Out = Ret7,V = 1 + V32,V32 >= 0,V33 >= 0,V1 = 1 + V33]). eq(minus(V, V1, Out),1,[],[Out = V34,V1 = 0,V = V34,V34 >= 0]). eq(minus(V, V1, Out),1,[],[Out = 0,V1 = V35,V35 >= 0,V = 0]). eq(minus(V, V1, Out),1,[minus(V36, V37, Ret8)],[Out = Ret8,V = 1 + V36,V36 >= 0,V37 >= 0,V1 = 1 + V37]). eq(plus(V, V1, Out),1,[plusIter(V38, V39, 0, Ret9)],[Out = Ret9,V = V38,V1 = V39,V38 >= 0,V39 >= 0]). eq(plusIter(V, V1, V4, Out),1,[le(V40, V41, Ret02),ifPlus(Ret02, V40, V42, V41, Ret10)],[Out = Ret10,V4 = V41,V41 >= 0,V = V40,V1 = V42,V40 >= 0,V42 >= 0]). eq(ifPlus(V, V1, V4, V8, Out),1,[],[Out = V43,V4 = V43,V44 >= 0,V = 2,V8 = V44,V45 >= 0,V43 >= 0,V1 = V45]). eq(ifPlus(V, V1, V4, V8, Out),1,[plusIter(V46, 1 + V47, 1 + V48, Ret12)],[Out = Ret12,V4 = V47,V48 >= 0,V8 = V48,V46 >= 0,V47 >= 0,V1 = V46,V = 1]). eq(a(Out),1,[],[Out = 0]). eq(a(Out),1,[],[Out = 1]). eq(inc(V, Out),0,[],[Out = 0,V49 >= 0,V = V49]). eq(le(V, V1, Out),0,[],[Out = 0,V50 >= 0,V51 >= 0,V1 = V51,V = V50]). eq(minus(V, V1, Out),0,[],[Out = 0,V52 >= 0,V53 >= 0,V1 = V53,V = V52]). eq(if1(V, V1, V4, V8, V9, V10, Out),0,[],[Out = 0,V8 = V54,V10 = V55,V56 >= 0,V57 >= 0,V4 = V58,V59 >= 0,V55 >= 0,V1 = V59,V9 = V57,V58 >= 0,V54 >= 0,V = V56]). eq(if2(V, V1, V4, V8, V9, Out),0,[],[Out = 0,V8 = V60,V61 >= 0,V62 >= 0,V4 = V63,V64 >= 0,V1 = V64,V9 = V62,V63 >= 0,V60 >= 0,V = V61]). eq(ifPlus(V, V1, V4, V8, Out),0,[],[Out = 0,V8 = V65,V66 >= 0,V4 = V67,V68 >= 0,V1 = V68,V67 >= 0,V65 >= 0,V = V66]). input_output_vars(div(V,V1,Out),[V,V1],[Out]). input_output_vars(div2(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(if1(V,V1,V4,V8,V9,V10,Out),[V,V1,V4,V8,V9,V10],[Out]). input_output_vars(if2(V,V1,V4,V8,V9,Out),[V,V1,V4,V8,V9],[Out]). input_output_vars(inc(V,Out),[V],[Out]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]). input_output_vars(plusIter(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(ifPlus(V,V1,V4,V8,Out),[V,V1,V4,V8],[Out]). input_output_vars(a(Out),[],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [a/1]
1. recursive : [minus/3]
2. recursive : [inc/2]
3. recursive : [le/3]
4. recursive : [ifPlus/5,plusIter/4]
5. non_recursive : [plus/3]
6. recursive : [div2/4,if1/7,if2/6]
7. non_recursive : [ (div)/3]
8. non_recursive : [start/6]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into a/1
1. SCC is partially evaluated into minus/3
2. SCC is partially evaluated into inc/2
3. SCC is partially evaluated into le/3
4. SCC is partially evaluated into plusIter/4
5. SCC is completely evaluated into other SCCs
6. SCC is partially evaluated into div2/4
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into start/6
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations a/1
* CE 37 is refined into CE [38]
* CE 36 is refined into CE [39]
### Cost equations --> "Loop" of a/1
* CEs [38] --> Loop 19
* CEs [39] --> Loop 20
### Ranking functions of CR a(Out)
#### Partial ranking functions of CR a(Out)
### Specialization of cost equations minus/3
* CE 17 is refined into CE [40]
* CE 18 is refined into CE [41]
* CE 20 is refined into CE [42]
* CE 19 is refined into CE [43]
### Cost equations --> "Loop" of minus/3
* CEs [43] --> Loop 21
* CEs [40] --> Loop 22
* CEs [41,42] --> Loop 23
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [21]: [V,V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [21]:
- RF of loop [21:1]:
V
V1
### Specialization of cost equations inc/2
* CE 29 is refined into CE [44]
* CE 31 is refined into CE [45]
* CE 30 is refined into CE [46]
### Cost equations --> "Loop" of inc/2
* CEs [46] --> Loop 24
* CEs [44,45] --> Loop 25
### Ranking functions of CR inc(V,Out)
* RF of phase [24]: [V]
#### Partial ranking functions of CR inc(V,Out)
* Partial RF of phase [24]:
- RF of loop [24:1]:
V
### Specialization of cost equations le/3
* CE 35 is refined into CE [47]
* CE 32 is refined into CE [48]
* CE 33 is refined into CE [49]
* CE 34 is refined into CE [50]
### Cost equations --> "Loop" of le/3
* CEs [50] --> Loop 26
* CEs [47] --> Loop 27
* CEs [48] --> Loop 28
* CEs [49] --> Loop 29
### Ranking functions of CR le(V,V1,Out)
* RF of phase [26]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [26]:
- RF of loop [26:1]:
V
V1
### Specialization of cost equations plusIter/4
* CE 28 is refined into CE [51,52]
* CE 26 is refined into CE [53,54,55,56,57]
* CE 27 is refined into CE [58,59]
### Cost equations --> "Loop" of plusIter/4
* CEs [59] --> Loop 30
* CEs [58] --> Loop 31
* CEs [52] --> Loop 32
* CEs [54] --> Loop 33
* CEs [51] --> Loop 34
* CEs [53,55,56,57] --> Loop 35
### Ranking functions of CR plusIter(V,V1,V4,Out)
* RF of phase [30]: [V-V4]
#### Partial ranking functions of CR plusIter(V,V1,V4,Out)
* Partial RF of phase [30]:
- RF of loop [30:1]:
V-V4
### Specialization of cost equations div2/4
* CE 25 is refined into CE [60,61,62,63,64,65,66,67,68,69,70,71,72,73]
* CE 21 is refined into CE [74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101]
* CE 22 is refined into CE [102,103,104,105,106,107,108,109,110,111,112,113,114,115]
* CE 24 is refined into CE [116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192]
* CE 23 is refined into CE [193,194,195,196,197,198,199,200,201,202,203,204,205,206]
### Cost equations --> "Loop" of div2/4
* CEs [206] --> Loop 36
* CEs [205] --> Loop 37
* CEs [198,202] --> Loop 38
* CEs [196] --> Loop 39
* CEs [197,201] --> Loop 40
* CEs [195] --> Loop 41
* CEs [194,200,204] --> Loop 42
* CEs [193,199,203] --> Loop 43
* CEs [114,115] --> Loop 44
* CEs [110,111] --> Loop 45
* CEs [81,88,95,109,137,144,151,172,179,186] --> Loop 46
* CEs [61,62,68,69] --> Loop 47
* CEs [117,118,124,125,159,160] --> Loop 48
* CEs [60,63,64,65,66,67,70,71,72,73] --> Loop 49
* CEs [116,119,120,121,122,123,126,127,128,129,158,161,162,163,164] --> Loop 50
* CEs [107,108] --> Loop 51
* CEs [103,104] --> Loop 52
* CEs [75,76,82,83,89,90,96,97,131,132,138,139,145,146,152,153,166,167,173,174,180,181,187,188] --> Loop 53
* CEs [74,77,78,79,80,84,85,86,87,91,92,93,94,98,99,100,101,102,105,106,112,113,130,133,134,135,136,140,141,142,143,147,148,149,150,154,155,156,157,165,168,169,170,171,175,176,177,178,182,183,184,185,189,190,191,192] --> Loop 54
### Ranking functions of CR div2(V,V1,V4,Out)
* RF of phase [36,38]: [V,V-V1+1]
* RF of phase [42]: [V,V-V1+1]
#### Partial ranking functions of CR div2(V,V1,V4,Out)
* Partial RF of phase [36,38]:
- RF of loop [36:1,38:1]:
V
V-V1+1
* Partial RF of phase [42]:
- RF of loop [42:1]:
V
V-V1+1
### Specialization of cost equations start/6
* CE 2 is refined into CE [207]
* CE 3 is refined into CE [208]
* CE 4 is refined into CE [209]
* CE 5 is refined into CE [210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228]
* CE 6 is refined into CE [229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247]
* CE 7 is refined into CE [248]
* CE 8 is refined into CE [249,250,251,252]
* CE 9 is refined into CE [253,254,255]
* CE 10 is refined into CE [256,257,258,259,260,261,262,263,264,265]
* CE 11 is refined into CE [266,267]
* CE 12 is refined into CE [268,269,270,271,272]
* CE 13 is refined into CE [273,274,275]
* CE 14 is refined into CE [276,277,278,279]
* CE 15 is refined into CE [280,281,282,283,284,285]
* CE 16 is refined into CE [286,287]
### Cost equations --> "Loop" of start/6
* CEs [207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287] --> Loop 55
### Ranking functions of CR start(V,V1,V4,V8,V9,V10)
#### Partial ranking functions of CR start(V,V1,V4,V8,V9,V10)
Computing Bounds
=====================================
#### Cost of chains of a(Out):
* Chain [20]: 1
with precondition: [Out=0]
* Chain [19]: 1
with precondition: [Out=1]
#### Cost of chains of minus(V,V1,Out):
* Chain [[21],23]: 1*it(21)+1
Such that:it(21) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[21],22]: 1*it(21)+1
Such that:it(21) =< V1
with precondition: [V=Out+V1,V1>=1,V>=V1]
* Chain [23]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [22]: 1
with precondition: [V1=0,V=Out,V>=0]
#### Cost of chains of inc(V,Out):
* Chain [[24],25]: 1*it(24)+1
Such that:it(24) =< Out
with precondition: [Out>=1,V>=Out]
* Chain [25]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of le(V,V1,Out):
* Chain [[26],29]: 1*it(26)+1
Such that:it(26) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[26],28]: 1*it(26)+1
Such that:it(26) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[26],27]: 1*it(26)+0
Such that:it(26) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [29]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [28]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [27]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of plusIter(V,V1,V4,Out):
* Chain [[30],35]: 3*it(30)+3*s(3)+1*s(8)+2
Such that:it(30) =< V-V4
aux(3) =< V
s(3) =< aux(3)
s(8) =< it(30)*aux(3)
with precondition: [Out=0,V1>=0,V4>=1,V>=V4+1]
* Chain [[30],32]: 3*it(30)+1*s(8)+1*s(9)+3
Such that:it(30) =< -V1+Out
aux(4) =< V
s(9) =< aux(4)
s(8) =< it(30)*aux(4)
with precondition: [V+V1=Out+V4,V1>=0,V4>=1,V>=V4+1]
* Chain [35]: 2*s(3)+1*s(5)+2
Such that:s(5) =< V
aux(1) =< V4
s(3) =< aux(1)
with precondition: [Out=0,V>=0,V1>=0,V4>=0]
* Chain [34]: 3
with precondition: [V=0,V1=Out,V1>=0,V4>=0]
* Chain [33]: 2
with precondition: [V4=0,Out=0,V>=1,V1>=0]
* Chain [32]: 1*s(9)+3
Such that:s(9) =< V
with precondition: [V1=Out,V>=1,V1>=0,V4>=V]
* Chain [31,[30],35]: 6*it(30)+1*s(8)+5
Such that:aux(5) =< V
it(30) =< aux(5)
s(8) =< it(30)*aux(5)
with precondition: [V4=0,Out=0,V>=2,V1>=0]
* Chain [31,[30],32]: 4*it(30)+1*s(8)+6
Such that:aux(6) =< -V1+Out
it(30) =< aux(6)
s(8) =< it(30)*aux(6)
with precondition: [V4=0,V+V1=Out,V>=2,V1>=0]
* Chain [31,35]: 2*s(3)+1*s(5)+5
Such that:aux(1) =< 1
s(5) =< V
s(3) =< aux(1)
with precondition: [V4=0,Out=0,V>=1,V1>=0]
* Chain [31,32]: 1*s(9)+6
Such that:s(9) =< 1
with precondition: [V=1,V4=0,Out=V1+1,Out>=1]
#### Cost of chains of div2(V,V1,V4,Out):
* Chain [[42],54]: 14*it(42)+56*s(28)+32*s(49)+12*s(109)+18*s(454)+2*s(455)+3*s(456)+12
Such that:aux(56) =< 1
aux(68) =< V-V1+1
aux(58) =< V1
aux(72) =< V
aux(73) =< V4
s(49) =< aux(72)
s(109) =< aux(58)
s(28) =< aux(56)
aux(66) =< aux(72)
it(42) =< aux(72)
aux(66) =< aux(68)
it(42) =< aux(68)
s(454) =< aux(73)
s(455) =< aux(66)
s(456) =< s(454)*aux(73)
with precondition: [Out=0,V1>=1,V4>=0,V>=V1]
* Chain [[42],46]: 14*it(42)+13*s(453)+18*s(454)+2*s(455)+3*s(456)+3*s(462)+10
Such that:aux(68) =< V-V1+1
aux(75) =< V1
aux(76) =< V
aux(77) =< V4
s(453) =< aux(76)
s(462) =< aux(75)
aux(66) =< aux(76)
it(42) =< aux(76)
aux(66) =< aux(68)
it(42) =< aux(68)
s(454) =< aux(77)
s(455) =< aux(66)
s(456) =< s(454)*aux(77)
with precondition: [Out=0,V1>=1,V4>=0,V>=V1]
* Chain [[42],43,54]: 14*it(42)+58*s(28)+18*s(109)+6*s(453)+18*s(454)+2*s(455)+3*s(456)+26
Such that:aux(85) =< 1
aux(67) =< V
aux(68) =< V-V1+1
aux(86) =< V1
aux(87) =< V-V1
aux(88) =< V4
s(109) =< aux(86)
s(28) =< aux(85)
aux(66) =< aux(67)
it(42) =< aux(67)
s(458) =< aux(67)
aux(66) =< aux(68)
it(42) =< aux(68)
aux(66) =< aux(87)
it(42) =< aux(87)
s(458) =< aux(87)
s(454) =< aux(88)
s(453) =< s(458)
s(455) =< aux(66)
s(456) =< s(454)*aux(88)
with precondition: [Out=0,V1>=1,V4>=0,V>=2*V1]
* Chain [[42],43,46]: 14*it(42)+6*s(453)+18*s(454)+2*s(455)+3*s(456)+9*s(462)+2*s(481)+24
Such that:s(476) =< 1
aux(67) =< V
aux(68) =< V-V1+1
aux(89) =< V1
aux(90) =< V-V1
aux(91) =< V4
s(462) =< aux(89)
s(481) =< s(476)
aux(66) =< aux(67)
it(42) =< aux(67)
s(458) =< aux(67)
aux(66) =< aux(68)
it(42) =< aux(68)
aux(66) =< aux(90)
it(42) =< aux(90)
s(458) =< aux(90)
s(454) =< aux(91)
s(453) =< s(458)
s(455) =< aux(66)
s(456) =< s(454)*aux(91)
with precondition: [Out=0,V1>=1,V4>=0,V>=2*V1]
* Chain [[36,38],[42],54]: 42*it(36)+56*s(28)+38*s(49)+12*s(109)+18*s(454)+6*s(455)+3*s(456)+18*s(528)+1*s(529)+2*s(530)+2*s(536)+12
Such that:aux(56) =< 1
aux(58) =< V1
aux(108) =< V
aux(109) =< V-V1+1
aux(110) =< V4
s(49) =< aux(108)
s(109) =< aux(58)
s(28) =< aux(56)
aux(66) =< aux(108)
it(36) =< aux(108)
aux(66) =< aux(109)
it(36) =< aux(109)
s(454) =< aux(110)
s(455) =< aux(66)
s(456) =< s(454)*aux(110)
aux(99) =< aux(110)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(110)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],[42],46]: 42*it(36)+13*s(453)+18*s(454)+12*s(455)+3*s(456)+3*s(462)+18*s(528)+1*s(529)+2*s(530)+2*s(536)+10
Such that:aux(75) =< V1
aux(111) =< V
aux(112) =< V-V1+1
aux(113) =< V4
s(453) =< aux(111)
s(462) =< aux(75)
aux(66) =< aux(111)
it(36) =< aux(111)
aux(66) =< aux(112)
it(36) =< aux(112)
s(454) =< aux(113)
s(455) =< aux(66)
s(456) =< s(454)*aux(113)
aux(99) =< aux(113)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(113)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],[42],43,54]: 28*it(36)+14*it(42)+58*s(28)+18*s(109)+6*s(453)+18*s(454)+2*s(455)+3*s(456)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+26
Such that:aux(85) =< 1
aux(87) =< V-V1
aux(86) =< V1
aux(114) =< V
aux(115) =< V-V1+1
aux(116) =< V4
s(109) =< aux(86)
s(28) =< aux(85)
aux(66) =< aux(114)
it(42) =< aux(114)
s(458) =< aux(114)
aux(66) =< aux(115)
it(42) =< aux(115)
aux(66) =< aux(87)
it(42) =< aux(87)
s(458) =< aux(87)
s(454) =< aux(116)
s(453) =< s(458)
s(455) =< aux(66)
s(456) =< s(454)*aux(116)
aux(101) =< aux(114)
it(36) =< aux(114)
aux(101) =< aux(115)
it(36) =< aux(115)
aux(99) =< aux(116)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< aux(114)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(116)
with precondition: [Out=0,V1>=1,V4>=1,V>=3*V1]
* Chain [[36,38],[42],43,46]: 28*it(36)+14*it(42)+6*s(453)+18*s(454)+2*s(455)+3*s(456)+9*s(462)+2*s(481)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+24
Such that:s(476) =< 1
aux(90) =< V-V1
aux(89) =< V1
aux(117) =< V
aux(118) =< V-V1+1
aux(119) =< V4
s(462) =< aux(89)
s(481) =< s(476)
aux(66) =< aux(117)
it(42) =< aux(117)
s(458) =< aux(117)
aux(66) =< aux(118)
it(42) =< aux(118)
aux(66) =< aux(90)
it(42) =< aux(90)
s(458) =< aux(90)
s(454) =< aux(119)
s(453) =< s(458)
s(455) =< aux(66)
s(456) =< s(454)*aux(119)
aux(101) =< aux(117)
it(36) =< aux(117)
aux(101) =< aux(118)
it(36) =< aux(118)
aux(99) =< aux(119)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< aux(117)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(119)
with precondition: [Out=0,V1>=1,V4>=1,V>=3*V1]
* Chain [[36,38],54]: 28*it(36)+514*s(24)+56*s(28)+80*s(29)+32*s(49)+12*s(109)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+12
Such that:aux(56) =< 1
aux(105) =< V-V1+1
aux(58) =< V1
aux(120) =< V
aux(121) =< V4
s(49) =< aux(120)
s(109) =< aux(58)
s(24) =< aux(121)
s(28) =< aux(56)
s(29) =< s(24)*aux(121)
aux(101) =< aux(120)
it(36) =< aux(120)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(99) =< aux(121)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(121)
with precondition: [Out=0,V1>=1,V4>=1,V>=V1]
* Chain [[36,38],53]: 28*it(36)+18*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+36*s(541)+6*s(554)+12
Such that:aux(134) =< 1
aux(105) =< V-V1+1
aux(136) =< V1
s(497) =< V4
aux(137) =< V
s(541) =< aux(134)
s(527) =< aux(137)
s(554) =< aux(136)
aux(101) =< aux(137)
it(36) =< aux(137)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=V1]
* Chain [[36,38],52]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+16
Such that:aux(105) =< V-V1+1
s(497) =< V4
aux(140) =< V
aux(101) =< aux(140)
it(36) =< aux(140)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< aux(140)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=1,V1>=1,V4>=1,V>=V1]
* Chain [[36,38],51]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+9*s(607)+2*s(608)+13
Such that:aux(105) =< V-V1+1
s(497) =< V4
aux(142) =< Out
aux(143) =< V
s(607) =< aux(142)
s(608) =< s(607)*aux(142)
aux(101) =< aux(143)
it(36) =< aux(143)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< aux(143)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [V1>=1,Out>=2,V>=V1,V4>=Out]
* Chain [[36,38],45]: 28*it(36)+8*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+3*s(614)+13
Such that:aux(145) =< 1
aux(105) =< V-V1+1
s(497) =< V4
aux(147) =< V
s(614) =< aux(145)
s(527) =< aux(147)
aux(101) =< aux(147)
it(36) =< aux(147)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=1,V1>=2,V4>=1,V>=V1+1]
* Chain [[36,38],44]: 28*it(36)+8*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+9*s(620)+2*s(621)+13
Such that:aux(105) =< V-V1+1
s(497) =< V4
aux(150) =< Out
aux(151) =< V
s(527) =< aux(151)
s(620) =< aux(150)
s(621) =< s(620)*aux(150)
aux(101) =< aux(151)
it(36) =< aux(151)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [V1>=2,Out>=2,V>=V1+1,V4>=Out]
* Chain [[36,38],43,54]: 28*it(36)+58*s(28)+18*s(109)+18*s(477)+3*s(482)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+26
Such that:aux(85) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(86) =< V1
aux(152) =< V-V1
aux(153) =< V4
s(109) =< aux(86)
s(28) =< aux(85)
s(477) =< aux(153)
s(482) =< s(477)*aux(153)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(152)
it(36) =< aux(152)
s(532) =< aux(152)
aux(99) =< aux(153)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(153)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],43,46]: 28*it(36)+9*s(462)+18*s(477)+2*s(481)+3*s(482)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+24
Such that:s(476) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(89) =< V1
aux(154) =< V-V1
aux(155) =< V4
s(462) =< aux(89)
s(477) =< aux(155)
s(481) =< s(476)
s(482) =< s(477)*aux(155)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(154)
it(36) =< aux(154)
s(532) =< aux(154)
aux(99) =< aux(155)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(155)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],41,54]: 28*it(36)+57*s(28)+14*s(109)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+26
Such that:aux(158) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(159) =< V1
s(497) =< V4
aux(160) =< V-V1
s(28) =< aux(158)
s(109) =< aux(159)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(160)
it(36) =< aux(160)
s(532) =< aux(160)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],41,46]: 28*it(36)+5*s(462)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+1*s(628)+24
Such that:s(628) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(161) =< V1
s(497) =< V4
aux(162) =< V-V1
s(462) =< aux(161)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(162)
it(36) =< aux(162)
s(532) =< aux(162)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],40,54]: 28*it(36)+529*s(24)+60*s(28)+82*s(29)+16*s(109)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+26
Such that:aux(169) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(170) =< V1
aux(172) =< V-V1
aux(173) =< V4
s(24) =< aux(173)
s(109) =< aux(170)
s(28) =< aux(169)
s(29) =< s(24)*aux(173)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(172)
it(36) =< aux(172)
s(532) =< aux(172)
aux(99) =< aux(173)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(173)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],40,53]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+41*s(541)+10*s(554)+14*s(636)+2*s(641)+26
Such that:aux(174) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(175) =< V1
aux(176) =< V-V1
aux(177) =< V4
s(541) =< aux(174)
s(554) =< aux(175)
s(636) =< aux(177)
s(641) =< s(636)*aux(177)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(176)
it(36) =< aux(176)
s(532) =< aux(176)
aux(99) =< aux(177)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(177)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],40,52]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+4*s(630)+5*s(631)+14*s(636)+2*s(641)+30
Such that:aux(178) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(168) =< V1
aux(179) =< V-V1
aux(180) =< V4
s(631) =< aux(178)
s(630) =< aux(168)
s(636) =< aux(180)
s(641) =< s(636)*aux(180)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(179)
it(36) =< aux(179)
s(532) =< aux(179)
aux(99) =< aux(180)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(180)
with precondition: [Out=1,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],40,51]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+10*s(607)+2*s(608)+4*s(630)+4*s(631)+14*s(636)+2*s(641)+27
Such that:aux(167) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(168) =< V1
aux(181) =< Out
aux(182) =< V-V1
aux(183) =< V4
s(607) =< aux(181)
s(608) =< s(607)*aux(181)
s(631) =< aux(167)
s(630) =< aux(168)
s(636) =< aux(183)
s(641) =< s(636)*aux(183)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(182)
it(36) =< aux(182)
s(532) =< aux(182)
aux(99) =< aux(183)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(183)
with precondition: [V1>=1,Out>=2,V>=2*V1,V4>=Out]
* Chain [[36,38],39,[42],54]: 28*it(36)+14*it(42)+57*s(28)+32*s(49)+14*s(109)+2*s(455)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+26
Such that:aux(185) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(186) =< V1
s(497) =< V4
aux(187) =< V-2*V1+1
aux(188) =< V-V1
s(28) =< aux(185)
s(49) =< aux(188)
s(109) =< aux(186)
aux(66) =< aux(188)
it(42) =< aux(188)
aux(66) =< aux(187)
it(42) =< aux(187)
s(455) =< aux(66)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(187)
it(36) =< aux(187)
aux(101) =< aux(188)
it(36) =< aux(188)
s(532) =< aux(188)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=3*V1]
* Chain [[36,38],39,[42],46]: 28*it(36)+14*it(42)+13*s(453)+2*s(455)+5*s(462)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+1*s(647)+24
Such that:s(647) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(189) =< V1
s(497) =< V4
aux(190) =< V-2*V1+1
aux(191) =< V-V1
s(453) =< aux(191)
s(462) =< aux(189)
aux(66) =< aux(191)
it(42) =< aux(191)
aux(66) =< aux(190)
it(42) =< aux(190)
s(455) =< aux(66)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(190)
it(36) =< aux(190)
aux(101) =< aux(191)
it(36) =< aux(191)
s(532) =< aux(191)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=3*V1]
* Chain [[36,38],39,[42],43,54]: 28*it(36)+14*it(42)+59*s(28)+20*s(109)+6*s(453)+2*s(455)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+40
Such that:aux(192) =< 1
aux(104) =< V
aux(67) =< V-V1
aux(105) =< V-V1+1
aux(193) =< V1
s(497) =< V4
aux(194) =< V-2*V1
aux(195) =< V-2*V1+1
s(28) =< aux(192)
s(109) =< aux(193)
aux(66) =< aux(67)
it(42) =< aux(67)
s(458) =< aux(67)
aux(66) =< aux(195)
it(42) =< aux(195)
aux(66) =< aux(194)
it(42) =< aux(194)
s(458) =< aux(194)
s(453) =< s(458)
s(455) =< aux(66)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(195)
it(36) =< aux(195)
aux(101) =< aux(194)
it(36) =< aux(194)
s(532) =< aux(194)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=4*V1]
* Chain [[36,38],39,[42],43,46]: 28*it(36)+14*it(42)+6*s(453)+2*s(455)+11*s(462)+3*s(481)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+38
Such that:aux(196) =< 1
aux(104) =< V
aux(67) =< V-V1
aux(105) =< V-V1+1
aux(197) =< V1
s(497) =< V4
aux(198) =< V-2*V1
aux(199) =< V-2*V1+1
s(481) =< aux(196)
s(462) =< aux(197)
aux(66) =< aux(67)
it(42) =< aux(67)
s(458) =< aux(67)
aux(66) =< aux(199)
it(42) =< aux(199)
aux(66) =< aux(198)
it(42) =< aux(198)
s(458) =< aux(198)
s(453) =< s(458)
s(455) =< aux(66)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(199)
it(36) =< aux(199)
aux(101) =< aux(198)
it(36) =< aux(198)
s(532) =< aux(198)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=4*V1]
* Chain [[36,38],39,54]: 28*it(36)+57*s(28)+26*s(49)+14*s(109)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+26
Such that:aux(200) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(201) =< V1
s(497) =< V4
aux(202) =< V-V1
s(28) =< aux(200)
s(49) =< aux(202)
s(109) =< aux(201)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(202)
it(36) =< aux(202)
s(532) =< aux(202)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],39,46]: 28*it(36)+7*s(460)+5*s(462)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+1*s(647)+24
Such that:s(647) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(203) =< V1
s(497) =< V4
aux(204) =< V-V1
s(460) =< aux(204)
s(462) =< aux(203)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(204)
it(36) =< aux(204)
s(532) =< aux(204)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=2*V1]
* Chain [[36,38],39,43,54]: 28*it(36)+59*s(28)+20*s(109)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+40
Such that:aux(205) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(206) =< V1
s(497) =< V4
aux(207) =< V-2*V1
s(28) =< aux(205)
s(109) =< aux(206)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(207)
it(36) =< aux(207)
s(532) =< aux(207)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=3*V1]
* Chain [[36,38],39,43,46]: 28*it(36)+11*s(462)+3*s(481)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+38
Such that:aux(208) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(209) =< V1
s(497) =< V4
aux(210) =< V-2*V1
s(481) =< aux(208)
s(462) =< aux(209)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(210)
it(36) =< aux(210)
s(532) =< aux(210)
aux(99) =< s(497)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*s(497)
with precondition: [Out=0,V1>=1,V4>=1,V>=3*V1]
* Chain [[36,38],37,54]: 28*it(36)+519*s(24)+56*s(28)+81*s(29)+14*s(109)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+26
Such that:aux(56) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(212) =< V1
aux(214) =< V-V1
aux(215) =< V4
s(24) =< aux(215)
s(109) =< aux(212)
s(28) =< aux(56)
s(29) =< s(24)*aux(215)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(214)
it(36) =< aux(214)
s(532) =< aux(214)
aux(99) =< aux(215)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(215)
with precondition: [Out=0,V1>=1,V4>=2,V>=2*V1]
* Chain [[36,38],37,53]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+37*s(541)+8*s(554)+4*s(651)+1*s(652)+26
Such that:aux(216) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(217) =< V1
aux(218) =< V-V1
aux(219) =< V4
s(541) =< aux(216)
s(554) =< aux(217)
s(651) =< aux(219)
s(652) =< s(651)*aux(219)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(218)
it(36) =< aux(218)
s(532) =< aux(218)
aux(99) =< aux(219)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(219)
with precondition: [Out=0,V1>=1,V4>=2,V>=2*V1]
* Chain [[36,38],37,52]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+2*s(649)+4*s(651)+1*s(652)+1*s(653)+30
Such that:s(653) =< 1
aux(104) =< V
aux(105) =< V-V1+1
aux(211) =< V1
aux(220) =< V-V1
aux(221) =< V4
s(649) =< aux(211)
s(651) =< aux(221)
s(652) =< s(651)*aux(221)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(220)
it(36) =< aux(220)
s(532) =< aux(220)
aux(99) =< aux(221)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(221)
with precondition: [Out=1,V1>=1,V4>=2,V>=2*V1]
* Chain [[36,38],37,51]: 28*it(36)+6*s(527)+18*s(528)+1*s(529)+2*s(530)+4*s(534)+2*s(536)+10*s(607)+2*s(608)+2*s(649)+4*s(651)+1*s(652)+27
Such that:aux(104) =< V
aux(105) =< V-V1+1
aux(211) =< V1
aux(222) =< Out
aux(223) =< V-V1
aux(224) =< V4
s(607) =< aux(222)
s(608) =< s(607)*aux(222)
s(649) =< aux(211)
s(651) =< aux(224)
s(652) =< s(651)*aux(224)
aux(101) =< aux(104)
it(36) =< aux(104)
s(532) =< aux(104)
aux(101) =< aux(105)
it(36) =< aux(105)
aux(101) =< aux(223)
it(36) =< aux(223)
s(532) =< aux(223)
aux(99) =< aux(224)
s(530) =< it(36)*aux(99)
s(531) =< it(36)*aux(99)
s(534) =< aux(101)
s(527) =< s(532)
s(528) =< s(531)
s(536) =< s(528)*aux(99)
s(529) =< s(528)*aux(224)
with precondition: [V1>=1,Out>=2,V>=2*V1,V4>=Out]
* Chain [54]: 514*s(24)+56*s(28)+80*s(29)+26*s(49)+12*s(109)+12
Such that:aux(56) =< 1
aux(57) =< V
aux(58) =< V1
aux(59) =< V4
s(49) =< aux(57)
s(109) =< aux(58)
s(24) =< aux(59)
s(28) =< aux(56)
s(29) =< s(24)*aux(59)
with precondition: [Out=0,V>=0,V1>=0,V4>=0]
* Chain [53]: 36*s(541)+12*s(544)+6*s(554)+12
Such that:aux(134) =< 1
aux(135) =< V
aux(136) =< V1
s(541) =< aux(134)
s(544) =< aux(135)
s(554) =< aux(136)
with precondition: [V4=1,Out=0,V>=0,V1>=0]
* Chain [52]: 16
with precondition: [V=0,V4=1,Out=1,V1>=1]
* Chain [51]: 9*s(607)+2*s(608)+13
Such that:aux(142) =< V4
s(607) =< aux(142)
s(608) =< s(607)*aux(142)
with precondition: [V=0,V4=Out,V1>=1,V4>=2]
* Chain [50]: 114*s(656)+12*s(660)+18*s(661)+5*s(681)+11
Such that:aux(236) =< 1
aux(237) =< V
aux(238) =< V4
s(681) =< aux(237)
s(656) =< aux(238)
s(660) =< aux(236)
s(661) =< s(656)*aux(238)
with precondition: [V1=0,Out=0,V>=0,V4>=0]
* Chain [49]: 76*s(744)+8*s(748)+12*s(749)+5*s(769)+12
Such that:aux(245) =< 1
aux(246) =< V
aux(247) =< V4
s(769) =< aux(246)
s(744) =< aux(247)
s(748) =< aux(245)
s(749) =< s(744)*aux(247)
with precondition: [V1=0,Out=1,V>=0,V4>=0]
* Chain [48]: 9*s(800)+2*s(803)+11
Such that:aux(251) =< 1
aux(252) =< V
s(800) =< aux(251)
s(803) =< aux(252)
with precondition: [V1=0,V4=1,Out=0,V>=0]
* Chain [47]: 6*s(813)+2*s(816)+12
Such that:aux(255) =< 1
aux(256) =< V
s(813) =< aux(255)
s(816) =< aux(256)
with precondition: [V1=0,V4=1,Out=1,V>=0]
* Chain [46]: 7*s(460)+3*s(462)+10
Such that:aux(74) =< V
aux(75) =< V1
s(460) =< aux(74)
s(462) =< aux(75)
with precondition: [V4=0,Out=0,V>=0,V1>=0]
* Chain [45]: 2*s(613)+3*s(614)+13
Such that:aux(145) =< 1
aux(146) =< V
s(614) =< aux(145)
s(613) =< aux(146)
with precondition: [V4=1,Out=1,V>=1,V1>=V+1]
* Chain [44]: 2*s(618)+9*s(620)+2*s(621)+13
Such that:aux(149) =< V
aux(150) =< V4
s(618) =< aux(149)
s(620) =< aux(150)
s(621) =< s(620)*aux(150)
with precondition: [V4=Out,V>=1,V4>=2,V1>=V+1]
* Chain [43,54]: 58*s(28)+18*s(109)+18*s(477)+3*s(482)+26
Such that:aux(82) =< V4
aux(85) =< 1
aux(86) =< V1
s(109) =< aux(86)
s(28) =< aux(85)
s(477) =< aux(82)
s(482) =< s(477)*aux(82)
with precondition: [Out=0,V1>=1,V4>=0,V>=V1]
* Chain [43,46]: 9*s(462)+18*s(477)+2*s(481)+3*s(482)+24
Such that:s(476) =< 1
aux(82) =< V4
aux(89) =< V1
s(462) =< aux(89)
s(477) =< aux(82)
s(481) =< s(476)
s(482) =< s(477)*aux(82)
with precondition: [Out=0,V1>=1,V4>=0,V>=V1]
* Chain [41,54]: 57*s(28)+14*s(109)+26
Such that:aux(158) =< 1
aux(159) =< V1
s(28) =< aux(158)
s(109) =< aux(159)
with precondition: [V4=1,Out=0,V1>=1,V>=V1]
* Chain [41,46]: 5*s(462)+1*s(628)+24
Such that:s(628) =< 1
aux(161) =< V1
s(462) =< aux(161)
with precondition: [V4=1,Out=0,V1>=1,V>=V1]
* Chain [40,54]: 529*s(24)+60*s(28)+82*s(29)+16*s(109)+26
Such that:aux(169) =< 1
aux(170) =< V1
aux(171) =< V4
s(24) =< aux(171)
s(109) =< aux(170)
s(28) =< aux(169)
s(29) =< s(24)*aux(171)
with precondition: [Out=0,V1>=1,V4>=1,V>=V1]
* Chain [40,53]: 41*s(541)+10*s(554)+14*s(636)+2*s(641)+26
Such that:aux(165) =< V4
aux(174) =< 1
aux(175) =< V1
s(541) =< aux(174)
s(554) =< aux(175)
s(636) =< aux(165)
s(641) =< s(636)*aux(165)
with precondition: [Out=0,V1>=1,V4>=1,V>=V1]
* Chain [40,52]: 4*s(630)+5*s(631)+14*s(636)+2*s(641)+30
Such that:aux(168) =< V1
aux(165) =< V4
aux(178) =< 1
s(631) =< aux(178)
s(630) =< aux(168)
s(636) =< aux(165)
s(641) =< s(636)*aux(165)
with precondition: [Out=1,V1>=1,V4>=1,V>=V1]
* Chain [40,51]: 10*s(607)+2*s(608)+4*s(630)+4*s(631)+14*s(636)+2*s(641)+27
Such that:aux(167) =< 1
aux(168) =< V1
aux(165) =< V4
aux(181) =< Out
s(607) =< aux(181)
s(608) =< s(607)*aux(181)
s(631) =< aux(167)
s(630) =< aux(168)
s(636) =< aux(165)
s(641) =< s(636)*aux(165)
with precondition: [V1>=1,Out>=2,V>=V1,V4>=Out]
* Chain [39,[42],54]: 14*it(42)+57*s(28)+32*s(49)+14*s(109)+2*s(455)+26
Such that:aux(68) =< V-2*V1+1
aux(72) =< V-V1
aux(185) =< 1
aux(186) =< V1
s(28) =< aux(185)
s(49) =< aux(72)
s(109) =< aux(186)
aux(66) =< aux(72)
it(42) =< aux(72)
aux(66) =< aux(68)
it(42) =< aux(68)
s(455) =< aux(66)
with precondition: [V4=1,Out=0,V1>=1,V>=2*V1]
* Chain [39,[42],46]: 14*it(42)+13*s(453)+2*s(455)+5*s(462)+1*s(647)+24
Such that:s(647) =< 1
aux(68) =< V-2*V1+1
aux(76) =< V-V1
aux(189) =< V1
s(453) =< aux(76)
s(462) =< aux(189)
aux(66) =< aux(76)
it(42) =< aux(76)
aux(66) =< aux(68)
it(42) =< aux(68)
s(455) =< aux(66)
with precondition: [V4=1,Out=0,V1>=1,V>=2*V1]
* Chain [39,[42],43,54]: 14*it(42)+59*s(28)+20*s(109)+6*s(453)+2*s(455)+40
Such that:aux(87) =< V-2*V1
aux(68) =< V-2*V1+1
aux(67) =< V-V1
aux(192) =< 1
aux(193) =< V1
s(28) =< aux(192)
s(109) =< aux(193)
aux(66) =< aux(67)
it(42) =< aux(67)
s(458) =< aux(67)
aux(66) =< aux(68)
it(42) =< aux(68)
aux(66) =< aux(87)
it(42) =< aux(87)
s(458) =< aux(87)
s(453) =< s(458)
s(455) =< aux(66)
with precondition: [V4=1,Out=0,V1>=1,V>=3*V1]
* Chain [39,[42],43,46]: 14*it(42)+6*s(453)+2*s(455)+11*s(462)+3*s(481)+38
Such that:aux(90) =< V-2*V1
aux(68) =< V-2*V1+1
aux(67) =< V-V1
aux(196) =< 1
aux(197) =< V1
s(481) =< aux(196)
s(462) =< aux(197)
aux(66) =< aux(67)
it(42) =< aux(67)
s(458) =< aux(67)
aux(66) =< aux(68)
it(42) =< aux(68)
aux(66) =< aux(90)
it(42) =< aux(90)
s(458) =< aux(90)
s(453) =< s(458)
s(455) =< aux(66)
with precondition: [V4=1,Out=0,V1>=1,V>=3*V1]
* Chain [39,54]: 57*s(28)+26*s(49)+14*s(109)+26
Such that:aux(57) =< V-V1
aux(200) =< 1
aux(201) =< V1
s(28) =< aux(200)
s(49) =< aux(57)
s(109) =< aux(201)
with precondition: [V4=1,Out=0,V1>=1,V>=V1]
* Chain [39,46]: 7*s(460)+5*s(462)+1*s(647)+24
Such that:s(647) =< 1
aux(74) =< V-V1
aux(203) =< V1
s(460) =< aux(74)
s(462) =< aux(203)
with precondition: [V4=1,Out=0,V1>=1,V>=V1]
* Chain [39,43,54]: 59*s(28)+20*s(109)+40
Such that:aux(205) =< 1
aux(206) =< V1
s(28) =< aux(205)
s(109) =< aux(206)
with precondition: [V4=1,Out=0,V1>=1,V>=2*V1]
* Chain [39,43,46]: 11*s(462)+3*s(481)+38
Such that:aux(208) =< 1
aux(209) =< V1
s(481) =< aux(208)
s(462) =< aux(209)
with precondition: [V4=1,Out=0,V1>=1,V>=2*V1]
* Chain [37,54]: 519*s(24)+56*s(28)+81*s(29)+14*s(109)+26
Such that:aux(56) =< 1
aux(212) =< V1
aux(213) =< V4
s(24) =< aux(213)
s(109) =< aux(212)
s(28) =< aux(56)
s(29) =< s(24)*aux(213)
with precondition: [Out=0,V1>=1,V4>=2,V>=V1]
* Chain [37,53]: 37*s(541)+8*s(554)+4*s(651)+1*s(652)+26
Such that:s(650) =< V4
aux(216) =< 1
aux(217) =< V1
s(541) =< aux(216)
s(554) =< aux(217)
s(651) =< s(650)
s(652) =< s(651)*s(650)
with precondition: [Out=0,V1>=1,V4>=2,V>=V1]
* Chain [37,52]: 2*s(649)+4*s(651)+1*s(652)+1*s(653)+30
Such that:s(653) =< 1
aux(211) =< V1
s(650) =< V4
s(649) =< aux(211)
s(651) =< s(650)
s(652) =< s(651)*s(650)
with precondition: [Out=1,V1>=1,V4>=2,V>=V1]
* Chain [37,51]: 10*s(607)+2*s(608)+2*s(649)+4*s(651)+1*s(652)+27
Such that:aux(211) =< V1
s(650) =< V4
aux(222) =< Out
s(607) =< aux(222)
s(608) =< s(607)*aux(222)
s(649) =< aux(211)
s(651) =< s(650)
s(652) =< s(651)*s(650)
with precondition: [V1>=1,Out>=2,V>=V1,V4>=Out]
#### Cost of chains of start(V,V1,V4,V8,V9,V10):
* Chain [55]: 12164*s(1670)+10779*s(1671)+1692*s(1673)+5293*s(1674)+840*s(1676)+44*s(1679)+126*s(1681)+396*s(1683)+44*s(1684)+22*s(1685)+1058*s(1758)+156*s(1798)+56*s(1800)+24*s(1802)+8*s(1803)+56*s(1813)+8*s(1814)+242*s(1881)+448*s(1883)+28*s(1886)+64*s(1888)+120*s(1889)+252*s(1890)+28*s(1891)+14*s(1892)+56*s(1894)+4*s(1896)+8*s(1898)+24*s(1899)+36*s(1900)+4*s(1901)+2*s(1902)+156*s(1903)+56*s(1905)+24*s(1907)+8*s(1908)+56*s(1910)+4*s(1911)+8*s(1913)+36*s(1914)+4*s(1915)+2*s(1916)+56*s(1918)+8*s(1919)+56*s(1921)+4*s(1922)+8*s(1924)+36*s(1925)+4*s(1926)+2*s(1927)+336*s(1929)+20*s(1930)+54*s(1932)+180*s(1933)+20*s(1934)+10*s(1935)+10779*s(2045)+1692*s(2047)+1457*s(2048)+840*s(2050)+44*s(2053)+126*s(2055)+396*s(2057)+44*s(2058)+22*s(2059)+156*s(2172)+56*s(2174)+24*s(2176)+8*s(2177)+56*s(2187)+8*s(2188)+242*s(2255)+448*s(2257)+28*s(2260)+64*s(2262)+120*s(2263)+252*s(2264)+28*s(2265)+14*s(2266)+56*s(2268)+4*s(2270)+8*s(2272)+24*s(2273)+36*s(2274)+4*s(2275)+2*s(2276)+156*s(2277)+56*s(2279)+24*s(2281)+8*s(2282)+56*s(2284)+4*s(2285)+8*s(2287)+36*s(2288)+4*s(2289)+2*s(2290)+56*s(2292)+8*s(2293)+56*s(2295)+4*s(2296)+8*s(2298)+36*s(2299)+4*s(2300)+2*s(2301)+336*s(2303)+20*s(2304)+54*s(2306)+180*s(2307)+20*s(2308)+10*s(2309)+6*s(2411)+1*s(2416)+2*s(2417)+2*s(2418)+491*s(2436)+784*s(2438)+112*s(2443)+216*s(2444)+112*s(2449)+16*s(2453)+48*s(2454)+234*s(2458)+84*s(2460)+36*s(2462)+12*s(2463)+112*s(2465)+16*s(2468)+84*s(2473)+12*s(2474)+112*s(2476)+16*s(2479)+560*s(2484)+92*s(2487)+586*s(2504)+28*s(2522)+252*s(2526)+28*s(2527)+14*s(2528)+4*s(2532)+36*s(2536)+4*s(2537)+2*s(2538)+4*s(2547)+36*s(2550)+4*s(2551)+2*s(2552)+4*s(2558)+36*s(2561)+4*s(2562)+2*s(2563)+20*s(2566)+180*s(2569)+20*s(2570)+10*s(2571)+5*s(2686)+6*s(2694)+2*s(2701)+43
Such that:s(2412) =< V8+1
aux(313) =< 1
aux(314) =< V
aux(315) =< V-2*V1
aux(316) =< V-2*V1+1
aux(317) =< V-V1
aux(318) =< V-V1+1
aux(319) =< V-V4
aux(320) =< V1
aux(321) =< V1+1
aux(322) =< V1-3*V4
aux(323) =< V1-3*V4+1
aux(324) =< V1-2*V4
aux(325) =< V1-2*V4+1
aux(326) =< V1-V4
aux(327) =< V1-V8
aux(328) =< -2*V4
aux(329) =< -2*V4+1
aux(330) =< -V4
aux(331) =< V4
aux(332) =< V4+1
aux(333) =< V4-3*V8
aux(334) =< V4-3*V8+1
aux(335) =< V4-2*V8
aux(336) =< V4-2*V8+1
aux(337) =< V4-V8
aux(338) =< -2*V8
aux(339) =< -2*V8+1
aux(340) =< -V8
aux(341) =< V8
aux(342) =< V9
aux(343) =< V10
s(1670) =< aux(313)
s(2436) =< aux(314)
s(2694) =< aux(319)
s(2048) =< aux(320)
s(2411) =< aux(327)
s(1674) =< aux(331)
s(1758) =< aux(341)
s(1671) =< aux(343)
s(1673) =< s(1671)*aux(343)
s(1675) =< aux(331)
s(1676) =< aux(331)
s(1675) =< aux(332)
s(1676) =< aux(332)
s(1678) =< aux(343)
s(1679) =< s(1676)*s(1678)
s(1680) =< s(1676)*s(1678)
s(1681) =< s(1675)
s(1683) =< s(1680)
s(1684) =< s(1683)*s(1678)
s(1685) =< s(1683)*aux(343)
s(1798) =< aux(340)
s(1799) =< aux(340)
s(1800) =< aux(340)
s(1801) =< aux(340)
s(1799) =< aux(339)
s(1800) =< aux(339)
s(1799) =< aux(338)
s(1800) =< aux(338)
s(1801) =< aux(338)
s(1802) =< s(1801)
s(1803) =< s(1799)
s(1812) =< aux(340)
s(1813) =< aux(340)
s(1812) =< aux(339)
s(1813) =< aux(339)
s(1814) =< s(1812)
s(1881) =< aux(337)
s(1882) =< aux(337)
s(1883) =< aux(337)
s(1884) =< aux(337)
s(1882) =< aux(336)
s(1883) =< aux(336)
s(1882) =< aux(335)
s(1883) =< aux(335)
s(1884) =< aux(335)
s(1886) =< s(1883)*s(1678)
s(1887) =< s(1883)*s(1678)
s(1888) =< s(1882)
s(1889) =< s(1884)
s(1890) =< s(1887)
s(1891) =< s(1890)*s(1678)
s(1892) =< s(1890)*aux(343)
s(1893) =< aux(337)
s(1894) =< aux(337)
s(1895) =< aux(337)
s(1893) =< aux(336)
s(1894) =< aux(336)
s(1893) =< aux(333)
s(1894) =< aux(333)
s(1895) =< aux(333)
s(1896) =< s(1894)*s(1678)
s(1897) =< s(1894)*s(1678)
s(1898) =< s(1893)
s(1899) =< s(1895)
s(1900) =< s(1897)
s(1901) =< s(1900)*s(1678)
s(1902) =< s(1900)*aux(343)
s(1903) =< aux(335)
s(1904) =< aux(335)
s(1905) =< aux(335)
s(1906) =< aux(335)
s(1904) =< aux(334)
s(1905) =< aux(334)
s(1904) =< aux(333)
s(1905) =< aux(333)
s(1906) =< aux(333)
s(1907) =< s(1906)
s(1908) =< s(1904)
s(1909) =< aux(337)
s(1910) =< aux(337)
s(1909) =< aux(336)
s(1910) =< aux(336)
s(1909) =< aux(334)
s(1910) =< aux(334)
s(1909) =< aux(333)
s(1910) =< aux(333)
s(1911) =< s(1910)*s(1678)
s(1912) =< s(1910)*s(1678)
s(1913) =< s(1909)
s(1914) =< s(1912)
s(1915) =< s(1914)*s(1678)
s(1916) =< s(1914)*aux(343)
s(1917) =< aux(335)
s(1918) =< aux(335)
s(1917) =< aux(334)
s(1918) =< aux(334)
s(1919) =< s(1917)
s(1920) =< aux(337)
s(1921) =< aux(337)
s(1920) =< aux(336)
s(1921) =< aux(336)
s(1920) =< aux(334)
s(1921) =< aux(334)
s(1920) =< aux(335)
s(1921) =< aux(335)
s(1922) =< s(1921)*s(1678)
s(1923) =< s(1921)*s(1678)
s(1924) =< s(1920)
s(1925) =< s(1923)
s(1926) =< s(1925)*s(1678)
s(1927) =< s(1925)*aux(343)
s(1928) =< aux(337)
s(1929) =< aux(337)
s(1928) =< aux(336)
s(1929) =< aux(336)
s(1930) =< s(1929)*s(1678)
s(1931) =< s(1929)*s(1678)
s(1932) =< s(1928)
s(1933) =< s(1931)
s(1934) =< s(1933)*s(1678)
s(1935) =< s(1933)*aux(343)
s(2045) =< aux(342)
s(2047) =< s(2045)*aux(342)
s(2049) =< aux(320)
s(2050) =< aux(320)
s(2049) =< aux(321)
s(2050) =< aux(321)
s(2052) =< aux(342)
s(2053) =< s(2050)*s(2052)
s(2054) =< s(2050)*s(2052)
s(2055) =< s(2049)
s(2057) =< s(2054)
s(2058) =< s(2057)*s(2052)
s(2059) =< s(2057)*aux(342)
s(2172) =< aux(330)
s(2173) =< aux(330)
s(2174) =< aux(330)
s(2175) =< aux(330)
s(2173) =< aux(329)
s(2174) =< aux(329)
s(2173) =< aux(328)
s(2174) =< aux(328)
s(2175) =< aux(328)
s(2176) =< s(2175)
s(2177) =< s(2173)
s(2186) =< aux(330)
s(2187) =< aux(330)
s(2186) =< aux(329)
s(2187) =< aux(329)
s(2188) =< s(2186)
s(2255) =< aux(326)
s(2256) =< aux(326)
s(2257) =< aux(326)
s(2258) =< aux(326)
s(2256) =< aux(325)
s(2257) =< aux(325)
s(2256) =< aux(324)
s(2257) =< aux(324)
s(2258) =< aux(324)
s(2260) =< s(2257)*s(2052)
s(2261) =< s(2257)*s(2052)
s(2262) =< s(2256)
s(2263) =< s(2258)
s(2264) =< s(2261)
s(2265) =< s(2264)*s(2052)
s(2266) =< s(2264)*aux(342)
s(2267) =< aux(326)
s(2268) =< aux(326)
s(2269) =< aux(326)
s(2267) =< aux(325)
s(2268) =< aux(325)
s(2267) =< aux(322)
s(2268) =< aux(322)
s(2269) =< aux(322)
s(2270) =< s(2268)*s(2052)
s(2271) =< s(2268)*s(2052)
s(2272) =< s(2267)
s(2273) =< s(2269)
s(2274) =< s(2271)
s(2275) =< s(2274)*s(2052)
s(2276) =< s(2274)*aux(342)
s(2277) =< aux(324)
s(2278) =< aux(324)
s(2279) =< aux(324)
s(2280) =< aux(324)
s(2278) =< aux(323)
s(2279) =< aux(323)
s(2278) =< aux(322)
s(2279) =< aux(322)
s(2280) =< aux(322)
s(2281) =< s(2280)
s(2282) =< s(2278)
s(2283) =< aux(326)
s(2284) =< aux(326)
s(2283) =< aux(325)
s(2284) =< aux(325)
s(2283) =< aux(323)
s(2284) =< aux(323)
s(2283) =< aux(322)
s(2284) =< aux(322)
s(2285) =< s(2284)*s(2052)
s(2286) =< s(2284)*s(2052)
s(2287) =< s(2283)
s(2288) =< s(2286)
s(2289) =< s(2288)*s(2052)
s(2290) =< s(2288)*aux(342)
s(2291) =< aux(324)
s(2292) =< aux(324)
s(2291) =< aux(323)
s(2292) =< aux(323)
s(2293) =< s(2291)
s(2294) =< aux(326)
s(2295) =< aux(326)
s(2294) =< aux(325)
s(2295) =< aux(325)
s(2294) =< aux(323)
s(2295) =< aux(323)
s(2294) =< aux(324)
s(2295) =< aux(324)
s(2296) =< s(2295)*s(2052)
s(2297) =< s(2295)*s(2052)
s(2298) =< s(2294)
s(2299) =< s(2297)
s(2300) =< s(2299)*s(2052)
s(2301) =< s(2299)*aux(342)
s(2302) =< aux(326)
s(2303) =< aux(326)
s(2302) =< aux(325)
s(2303) =< aux(325)
s(2304) =< s(2303)*s(2052)
s(2305) =< s(2303)*s(2052)
s(2306) =< s(2302)
s(2307) =< s(2305)
s(2308) =< s(2307)*s(2052)
s(2309) =< s(2307)*aux(342)
s(2416) =< s(2048)*aux(320)
s(2417) =< s(2412)
s(2418) =< s(2411)*aux(320)
s(2437) =< aux(314)
s(2438) =< aux(314)
s(2439) =< aux(314)
s(2437) =< aux(318)
s(2438) =< aux(318)
s(2437) =< aux(317)
s(2438) =< aux(317)
s(2439) =< aux(317)
s(2443) =< s(2437)
s(2444) =< s(2439)
s(2448) =< aux(314)
s(2449) =< aux(314)
s(2450) =< aux(314)
s(2448) =< aux(318)
s(2449) =< aux(318)
s(2448) =< aux(315)
s(2449) =< aux(315)
s(2450) =< aux(315)
s(2453) =< s(2448)
s(2454) =< s(2450)
s(2458) =< aux(317)
s(2459) =< aux(317)
s(2460) =< aux(317)
s(2461) =< aux(317)
s(2459) =< aux(316)
s(2460) =< aux(316)
s(2459) =< aux(315)
s(2460) =< aux(315)
s(2461) =< aux(315)
s(2462) =< s(2461)
s(2463) =< s(2459)
s(2464) =< aux(314)
s(2465) =< aux(314)
s(2464) =< aux(318)
s(2465) =< aux(318)
s(2464) =< aux(316)
s(2465) =< aux(316)
s(2464) =< aux(315)
s(2465) =< aux(315)
s(2468) =< s(2464)
s(2472) =< aux(317)
s(2473) =< aux(317)
s(2472) =< aux(316)
s(2473) =< aux(316)
s(2474) =< s(2472)
s(2475) =< aux(314)
s(2476) =< aux(314)
s(2475) =< aux(318)
s(2476) =< aux(318)
s(2475) =< aux(316)
s(2476) =< aux(316)
s(2475) =< aux(317)
s(2476) =< aux(317)
s(2479) =< s(2475)
s(2483) =< aux(314)
s(2484) =< aux(314)
s(2483) =< aux(318)
s(2484) =< aux(318)
s(2487) =< s(2483)
s(2504) =< s(1674)*aux(331)
s(2521) =< aux(331)
s(2522) =< s(2438)*s(2521)
s(2523) =< s(2438)*s(2521)
s(2526) =< s(2523)
s(2527) =< s(2526)*s(2521)
s(2528) =< s(2526)*aux(331)
s(2532) =< s(2449)*s(2521)
s(2533) =< s(2449)*s(2521)
s(2536) =< s(2533)
s(2537) =< s(2536)*s(2521)
s(2538) =< s(2536)*aux(331)
s(2547) =< s(2465)*s(2521)
s(2548) =< s(2465)*s(2521)
s(2550) =< s(2548)
s(2551) =< s(2550)*s(2521)
s(2552) =< s(2550)*aux(331)
s(2558) =< s(2476)*s(2521)
s(2559) =< s(2476)*s(2521)
s(2561) =< s(2559)
s(2562) =< s(2561)*s(2521)
s(2563) =< s(2561)*aux(331)
s(2566) =< s(2484)*s(2521)
s(2567) =< s(2484)*s(2521)
s(2569) =< s(2567)
s(2570) =< s(2569)*s(2521)
s(2571) =< s(2569)*aux(331)
s(2686) =< s(2436)*aux(314)
s(2701) =< s(2694)*aux(314)
with precondition: []
Closed-form bounds of start(V,V1,V4,V8,V9,V10):
-------------------------------------
* Chain [55] with precondition: []
- Upper bound: nat(V)*2687+12207+nat(V)*5*nat(V)+nat(V)*2*nat(V-V4)+nat(V1)*2423+nat(V1)*nat(V1)+nat(V1)*2*nat(V1-V8)+nat(V4)*6259+nat(V4)*600*nat(V)+nat(V4)*586*nat(V4)+nat(V4)*90*nat(V4)*nat(V)+nat(V8)*1058+nat(V9)*10779+nat(V9)*440*nat(V1)+nat(V9)*1692*nat(V9)+nat(V9)*66*nat(V9)*nat(V1)+nat(V9)*90*nat(V9)*nat(V1-V4)+nat(V9)*600*nat(V1-V4)+nat(V10)*10779+nat(V10)*440*nat(V4)+nat(V10)*1692*nat(V10)+nat(V10)*66*nat(V10)*nat(V4)+nat(V10)*90*nat(V10)*nat(V4-V8)+nat(V10)*600*nat(V4-V8)+nat(-V4)*308+nat(-V8)*308+nat(V8+1)*2+nat(V-V1)*462+nat(V-V4)*6+nat(V1-V4)*1480+nat(V1-V8)*6+nat(V1-2*V4)*308+nat(V4-V8)*1480+nat(V4-2*V8)*308
- Complexity: n^3
### Maximum cost of start(V,V1,V4,V8,V9,V10): nat(V)*2687+12207+nat(V)*5*nat(V)+nat(V)*2*nat(V-V4)+nat(V1)*2423+nat(V1)*nat(V1)+nat(V1)*2*nat(V1-V8)+nat(V4)*6259+nat(V4)*600*nat(V)+nat(V4)*586*nat(V4)+nat(V4)*90*nat(V4)*nat(V)+nat(V8)*1058+nat(V9)*10779+nat(V9)*440*nat(V1)+nat(V9)*1692*nat(V9)+nat(V9)*66*nat(V9)*nat(V1)+nat(V9)*90*nat(V9)*nat(V1-V4)+nat(V9)*600*nat(V1-V4)+nat(V10)*10779+nat(V10)*440*nat(V4)+nat(V10)*1692*nat(V10)+nat(V10)*66*nat(V10)*nat(V4)+nat(V10)*90*nat(V10)*nat(V4-V8)+nat(V10)*600*nat(V4-V8)+nat(-V4)*308+nat(-V8)*308+nat(V8+1)*2+nat(V-V1)*462+nat(V-V4)*6+nat(V1-V4)*1480+nat(V1-V8)*6+nat(V1-2*V4)*308+nat(V4-V8)*1480+nat(V4-2*V8)*308
Asymptotic class: n^3
* Total analysis performed in 8105 ms.